R-pre-init(i;ds;init;a;T;P)
== @i precondition for a(v:T):P State(ds) v  xfpf-domain(ds).@i x initially init(x):ds(x) 

latex

---

clarification:

R-pre-init(i;ds;init;a;T;P)
== @i precondition for a(v:T):
== @i P State(ds) v
==  xfpf-domain(ds).@i x initially fpf-ap(init; IdDeq; x):fpf-ap(ds; IdDeq; x) 

latex

Definitions	left  right, @loc precondition for a(v:T):P State(ds) v, xL.R(x), fpf-domain(f), @loc x initially v:T, f(x), IdDeq
FDL editor aliases	R-pre-init